theory GPTEE_Instantiation
  imports "./APIS_Req/APIs_Memory" 
          "./APIS_Req/APIs_TEE_IPC" 
          "./APIS_Req/APIs_TEEC_IPC" 
          "../GPTEE_SecurityModel/SecurityObjects/GPTEE_Objectives"

begin
section "New Definitions"

subsection "Utility Functions"

definition get_TA_domain :: "State⇒TA_State_Type⇒DOMAIN_ID" where
        "get_TA_domain s ta ≡ (SOME tid.  (the ((TAs_state s) tid)) = ta)"

primrec getTAOffset ::"TA_CONF⇒OFFSET" where
      "getTAOffset (TAConf _ _ _ _ offs _) = offs"

definition getTAInstanceTime::"Sys_Config⇒State⇒TA_UUID_TYPE⇒nat"where
  "getTAInstanceTime sc s tid ≡ system_time s + getTAOffset (the (TA_conf sc tid))" 

primrec getTAUUID::"TA_CONF⇒TA_UUID_TYPE"where
        "getTAUUID (TAConf uuid _ _ _ _ _) = uuid"

(*
definition getTAbyId::"State⇒tid⇒TA_State_Type"where
        "getTAbyId s tid ≡the (TAs s tid)"

definition getIdbyTA::"State⇒TA_State_Type⇒tid"where
        "getIdbyTA s ta ≡ SOME tid1. getTAbyId s tid1 = ta"

definition getTAStateByid::"State⇒tid⇒TA_mode_type"where
  "getTAStateByid s tid ≡ TA_mode (the (TAs s tid))"
       
definition Abort::"State⇒tid⇒State"where
        "Abort s tid ≡ let ta = TAs s; tastate = the (ta tid) in s⦇TAs := ta(tid := Some (tastate⦇TA_mode := Dead⦈))⦈"

definition Close_Instance::"State⇒tid⇒State"where
        "Close_Instance s tid ≡ let ta = TAs s; tastate = the (ta tid) in s⦇TAs := ta(tid := Some (tastate⦇TA_mode := Dead⦈))⦈"

definition Close_Session::"State⇒tid⇒session_id⇒State"where
        "Close_Session s tid sid ≡ let ta = TAs s; tastate = the (ta tid); tasession = TA_sessions tastate; sesstate = the (tasession sid) 
           in s⦇TAs := ta(tid := Some (tastate⦇TA_sessions := tasession(sid := Some  (sesstate⦇session_mode := Closed⦈))⦈))⦈"



definition getTABinaryCode::"State⇒tid⇒binary"where
"getTABinaryCode s tid ≡ TA_code (the (TAs s tid))"

definition getCheckCode::"State⇒key"where
  "getCheckCode s ≡ checkcode s"
 
*)

subsection "Event specification"

(*tee's default block id is 0 ,stands for tee's own executing space, cant be access by others*)
definition system_init :: "Sys_Config ⇒ State" where
    "system_init sc ≡ ⦇ current =  REE sc,
                        TAs_state = (λ x. None),
                        REE_state = ⦇driver_mem = [],tee_ctx_list=[],ree_total_size =DefaultREESize sc ⦈,
                        TEE_state = ⦇ta_mgr=⦇mgr_ta_sessions =[],mgr_ta_instances=[],BIDpointer=2⦈,tee_ree_ipc_driver =0,
                                    zircon=⦇property=(λx. None)⦈,
                                    tee_memories=[⦇block_id = 0,size=tee_own_size,ownership=TEE sc,access_right=(λx. None)((TEE sc):=Some READWRITE),is_SecureMem = True,related = None⦈],
                                    tee_total_size =DefaultTEESize sc - tee_own_size⦈,
                        system_time = 0,
                        exec_prime =[]
                      ⦈"

section "Instantiation"



consts sysconf :: "Sys_Config" 

definition sys_config_witness :: Sys_Config where              
"
sys_config_witness ≡ ⦇ REE = 0,
                       TEE = 1,
                       TA_conf = (λ x. None),
                       checkcode = 100,
                       TEE_name =0,
                       DefaultREESize = 100,
                       DefaultTEESize = 100
                      ⦈
"

definition TA_domain1 :: "State⇒TA_State_Type⇒DOMAIN_ID" where
        "TA_domain1 s ta ≡ get_TA_domain s ta"

specification (sysconf)
  ta_id_conf: "∀uuid. (TA_conf sysconf) uuid ≠ None ⟶ getTAUUID (the ((TA_conf sysconf) uuid)) = uuid"
  tee_no_ree: "TEE sysconf ≠REE sysconf"
  ta_ne_tee: "(TA_conf sysconf) x ≠None⟹x ≠ (TEE sysconf)"
  ta_no_ree: "(TA_conf sysconf) x ≠None⟹x ≠ (REE sysconf)" 
  tee_no_ta: "x = (TEE sysconf)⟹(TA_conf sysconf) x = None"
  ree_no_ta: "x = (REE sysconf)⟹(TA_conf sysconf) x = None"
  apply (intro exI[of _ "sys_config_witness"] allI impI, simp)
  apply (rule conjI, simp add: sys_config_witness_def)
  apply (rule conjI, simp add: sys_config_witness_def)
  apply (simp add: sys_config_witness_def)
  done

 (* "∀s ta. get_TA_domain s ta ≠ (TEE sysconf) ∧ get_TA_domain s ta ≠ (REE sysconf)"
  "∀s. inj (get_TA_domain s)"
  "∀d s. d = TEE sysconf ∨ d = REE sysconf ∨ (∃ta. get_TA_domain s ta = d)" *)


consts s0t :: State
definition s0t_witness :: State
  where "s0t_witness ≡ system_init sysconf"

specification (s0t) 
  s0t_init: "s0t = system_init sysconf"
  by simp



datatype Hypercall =TEEC_INITIALIZECONTEXT TEE_NAME "TEEC_CONTEXT_TYPE option"
                |TEEC_FINALIZECONTEXT "TEEC_CONTEXT_TYPE option"
                |TEEC_OPENSESSION1 "TEEC_CONTEXT_TYPE option" "TEEC_SESSION_TYPE option"
                                TA_UUID_TYPE Connection_Method Connection_Data "TEEC_Operation option" "(MemBlock × TEEC_MEMREF_TYPE)"
                |TEEC_OPENSESSION2
                |TEEC_OPENSESSION3 SESSION_ID_TYPE
                |TEEC_OPENSESSION4 
                |TEEC_CLOSESESSION1 FD_TYPE "SESSION_ID_TYPE option" PARAMS_TYPE PARAMS_TYPE
                |TEEC_CLOSESESSION2
                |TEEC_CLOSESESSION3
                |TEEC_CLOSESESSION4
                |TEEC_INVOKECOMMAND1 "SESSION_ID_TYPE option"  TIMEOUT_TYPE COMMAND_ID_TYPE PARAMS_TYPE PARAMS_TYPE "MemBlock × TEEC_MEMREF_TYPE"
                |TEEC_INVOKECOMMAND2
                |TEEC_INVOKECOMMAND3
                |TEEC_INVOKECOMMAND4
                |TEEC_REGISTERSHAREDMEMORY TEEC_CONTEXT_TYPE  TEEC_SharedMemory
                |TEEC_ALLOCATESHAREDMEMORY TEEC_CONTEXT_TYPE  TEEC_SharedMemory
                |TEEC_RELEASESHAREDMEMORY TEEC_SharedMemory
                |TEE_OPENTASESSION1 
                |TEE_OPENTASESSION2
                |TEE_OPENTASESSION3 SESSION_ID_TYPE
                |TEE_OPENTASESSION4
                |TEE_INVOKETACOMMAND1 "MemBlock × TEEC_MEMREF_TYPE"
                |TEE_INVOKETACOMMAND2
                |TEE_INVOKETACOMMAND3
                |TEE_INVOKETACOMMAND4
                |TEE_CLOSETASESSION1
                |TEE_CLOSETASESSION2
                |TEE_CLOSETASESSION3
                |TEE_CLOSETASESSION4
                |TEE_CHECKMEMORYACCESSRIGHTS accessFlags  MemBlock  BUFFER_SIZE_TYPE
                |TEE_MALLOC BUFFER_SIZE_TYPE hint
                |TEE_REALLOC MemBlock BUFFER_SIZE_TYPE
                |TEE_FREE MemBlock

datatype Syscall = Reserved

datatype Event = hyperc Hypercall|sys Syscall
(*
definition exec_event :: "Event ⇒ (State × State) set" where
      "exec_event e ≡ {(s,s'). s'∈ (let s1= 
                                      (
                                      let ep = exec_prime s in 
                                      if ep = [] 
                                          then s 
                                      else if (snd (snd (hd ep))) = TA_MEM_INIT 
                                          then (fst (TA_Memory_Init s sysconf (fst (hd ep)) (fst (snd (hd ep)))))  
                                      else (fst (TA_Memory_Init s sysconf (fst (hd ep)) (fst (snd (hd ep)))))  
                                      )
            in (case e of 
           hyperc (TEEC_INITIALIZECONTEXT tn tctext) ⇒{fst (TEEC_InitializeContext sysconf s1 tn tctext)}|
           hyperc (TEEC_FINALIZECONTEXT tctext) ⇒ {(TEEC_FinalizeContext sysconf s1 tctext)}|
           hyperc (TEEC_OPENSESSION tctext tcsession uuid cm cd tcop) ⇒{fst (TEEC_OpenSession sysconf s1 tctext tcsession uuid cm cd tcop)}|
           
           hyperc (TEEC_INVOKECOMMAND sid tt cid pt1 pt2) ⇒{fst (TEEC_InvokeCommand sysconf s1 sid tt cid pt1 pt2)}|
           
           hyperc (TEE_INVOKETACOMMAND sid tt cid pt1 pt2) ⇒{fst (TEE_InvokeTACommand sysconf s1 sid tt cid pt1 pt2)}|
           
           
           
            
       _ ⇒{s} ))} 
      "
*)



(*
definition exec_event :: "Event ⇒ (State × State) set" where
      "exec_event e ≡ {(s,s'). s'∈  (case e of 
           hyperc (TEEC_INITIALIZECONTEXT tn tctext) ⇒{fst (TEEC_InitializeContext sysconf s tn tctext)}|
           hyperc (TEEC_FINALIZECONTEXT tctext) ⇒ {(TEEC_FinalizeContext sysconf s tctext)}|
           hyperc (TEEC_OPENSESSION1 tct tst uuid cm cd opt mem_t) ⇒{fst(TEEC_OpenSession1 sysconf s tct tst uuid cm cd opt mem_t)}|
           hyperc TEEC_OPENSESSION2 ⇒{fst (TEEC_OpenSession2 sysconf s)}|
           hyperc (TEEC_OPENSESSION3 ses_id)⇒{fst (TEEC_OpenSession3 sysconf s ses_id)}|
           hyperc (TEEC_OPENSESSION4 res)⇒{fst (TEEC_OpenSession4 sysconf s res)}|
           hyperc (TEEC_CLOSESESSION1 fd ses_id pt1 pt2) ⇒{fst (TEEC_CloseSession1 sysconf s fd ses_id pt1 pt2)}|
           hyperc TEEC_CLOSESESSION2 ⇒{fst (TEEC_CloseSession2 sysconf s)}|
           hyperc TEEC_CLOSESESSION3 ⇒{fst (TEEC_CloseSession3 sysconf s)}|
           hyperc (TEEC_INVOKECOMMAND1 ses_id timeout cmd pt1 pt2 mem_t) ⇒{fst (TEEC_InvokeCommand1 sysconf s ses_id timeout cmd pt1 pt2 mem_t)}|
           hyperc TEEC_INVOKECOMMAND2⇒{fst (TEEC_InvokeCommand2 sysconf s)}|
           hyperc TEEC_INVOKECOMMAND3⇒{fst (TEEC_InvokeCommand3 sysconf s)}|
           hyperc (TEE_INVOKETACOMMAND1 mem_t)⇒{fst (TEE_InvokeTACommand1 sysconf s mem_t)}|
           hyperc TEE_INVOKETACOMMAND2⇒{fst (TEE_InvokeTACommand2 sysconf s)}|
           hyperc TEE_INVOKETACOMMAND3⇒{fst (TEE_InvokeTACommand3 sysconf s)}|
           hyperc TEE_CLOSETASESSION1⇒{fst (TEE_CloseTASession1 sysconf s)}|
           hyperc TEE_CLOSETASESSION2⇒{fst (TEE_CloseTASession2 sysconf s)}|
           hyperc TEE_CLOSETASESSION3⇒{fst (TEE_CloseTASession3 sysconf s)}|
           hyperc TEE_OPENTASESSION1 ⇒{fst (TEE_OpenTASession1 sysconf s)}|
           hyperc TEE_OPENTASESSION2⇒{fst (TEE_OpenTASession2 sysconf s)}|
           hyperc (TEE_OPENTASESSION3 sid)⇒{fst (TEE_OpenTASession3 sysconf s sid)}|
           hyperc (TEE_OPENTASESSION4 res)⇒{fst (TEE_OpenTASession4 sysconf s res)}|
           hyperc (TEE_CHECKMEMORYACCESSRIGHTS accessflags  bid bsize) ⇒{s}|
           hyperc (TEE_MALLOC bsize hi) ⇒{(TEE_Malloc sysconf s bsize hi)}|
           hyperc (TEE_REALLOC mb bsize) ⇒{(TEE_Realloc sysconf s mb bsize)}|
           hyperc (TEE_FREE bid) ⇒{(TEE_Free sysconf s bid)}|
           hyperc (TEEC_REGISTERSHAREDMEMORY tctext shared) ⇒{fst (TEEC_RegisterSharedMemory sysconf s tctext shared)}|
           hyperc (TEEC_ALLOCATESHAREDMEMORY tctext shared) ⇒{fst (TEEC_AllocateSharedMemory sysconf s tctext shared)}|
           hyperc (TEEC_RELEASESHAREDMEMORY shared) ⇒{(TEEC_ReleaseSharedMemory sysconf s shared)}|
   
 _ ⇒{s} )} 
      "
*)

definition exec_event :: "Event ⇒ (State × State) set" where
      "exec_event e ≡ {(s,s'). s'∈  (case e of 
           hyperc (TEEC_INITIALIZECONTEXT tn tctext) ⇒{fst (TEEC_InitializeContext sysconf s tn tctext)}|
           hyperc (TEEC_FINALIZECONTEXT tctext) ⇒ {(TEEC_FinalizeContext sysconf s tctext)}|
           hyperc (TEEC_OPENSESSION1 tct tst uuid cm cd opt mem_t) ⇒{fst(TEEC_OpenSession1 sysconf s tct tst uuid cm cd opt mem_t)}|
           hyperc TEEC_OPENSESSION2 ⇒{fst (TEEC_OpenSession2 sysconf s)}|
           hyperc (TEEC_OPENSESSION3 ses_id)⇒{fst (TEEC_OpenSession3 sysconf s ses_id)}|
           hyperc (TEEC_OPENSESSION4)⇒{fst (TEEC_OpenSession4 sysconf s)}|
           hyperc TEE_OPENTASESSION1 ⇒{fst (TEE_OpenTASession1 sysconf s)}|
           hyperc TEE_OPENTASESSION2⇒{fst (TEE_OpenTASession2 sysconf s)}|
           hyperc (TEE_OPENTASESSION3 sid)⇒{fst (TEE_OpenTASession3 sysconf s sid)}|
           hyperc (TEE_OPENTASESSION4)⇒{fst (TEE_OpenTASession4 sysconf s)}|
           hyperc (TEEC_CLOSESESSION1 fd ses_id pt1 pt2) ⇒{fst (TEEC_CloseSession1 sysconf s fd ses_id pt1 pt2)}|
           hyperc TEEC_CLOSESESSION2 ⇒{fst (TEEC_CloseSession2 sysconf s)}|
           hyperc TEEC_CLOSESESSION3 ⇒{fst (TEEC_CloseSession3 sysconf s)}|
           hyperc TEEC_CLOSESESSION4 ⇒{fst (TEEC_CloseSession4 sysconf s)}|
           hyperc TEE_CLOSETASESSION1⇒{fst (TEE_CloseTASession1 sysconf s)}|
           hyperc TEE_CLOSETASESSION2⇒{fst (TEE_CloseTASession2 sysconf s)}|
           hyperc TEE_CLOSETASESSION3⇒{fst (TEE_CloseTASession3 sysconf s)}|
           hyperc TEE_CLOSETASESSION4⇒{fst (TEE_CloseTASession4 sysconf s)}|
           hyperc (TEEC_INVOKECOMMAND1 ses_id timeout cmd pt1 pt2 mem_t) ⇒{fst (TEEC_InvokeCommand1 sysconf s ses_id timeout cmd pt1 pt2 mem_t)}|
           hyperc TEEC_INVOKECOMMAND2⇒{fst (TEEC_InvokeCommand2 sysconf s)}|
           hyperc TEEC_INVOKECOMMAND3⇒{fst (TEEC_InvokeCommand3 sysconf s)}|
           hyperc TEEC_INVOKECOMMAND4⇒{fst (TEEC_InvokeCommand4 sysconf s)}|
           hyperc (TEE_INVOKETACOMMAND1 mem_t)⇒{fst (TEE_InvokeTACommand1 sysconf s mem_t)}|
           hyperc TEE_INVOKETACOMMAND2⇒{fst (TEE_InvokeTACommand2 sysconf s)}|
           hyperc TEE_INVOKETACOMMAND3⇒{fst (TEE_InvokeTACommand3 sysconf s)}|
           hyperc TEE_INVOKETACOMMAND4⇒{fst (TEE_InvokeTACommand4 sysconf s)}|
           hyperc (TEE_CHECKMEMORYACCESSRIGHTS accessflags  bid bsize) ⇒{s}|
           hyperc (TEE_MALLOC bsize hi) ⇒{(TEE_Malloc sysconf s bsize hi)}|
           hyperc (TEE_REALLOC mb bsize) ⇒{(TEE_Realloc sysconf s mb bsize)}|
           hyperc (TEE_FREE bid) ⇒{(TEE_Free sysconf s bid)}|
           hyperc (TEEC_REGISTERSHAREDMEMORY tctext shared) ⇒{fst (TEEC_RegisterSharedMemory sysconf s tctext shared)}|
           hyperc (TEEC_ALLOCATESHAREDMEMORY tctext shared) ⇒{fst (TEEC_AllocateSharedMemory sysconf s tctext shared)}|
           hyperc (TEEC_RELEASESHAREDMEMORY shared) ⇒{(TEEC_ReleaseSharedMemory sysconf s shared)}|
   
 _ ⇒{s} )} 
      "


subsection "ISOLATION Instantiation"


definition domain_of_event :: "State ⇒ Event ⇒ DOMAIN_ID option" where 
    "domain_of_event s e ≡ Some (current s)"
(*
 hyperc (TEEC_INITIALIZECONTEXT _ _) ⇒Some (REE sysconf) |
      hyperc (TEEC_OPENSESSION _ _ _ _ _ _) ⇒Some (REE sysconf)|
*)

(*
definition get_exec_prime::"State⇒(EVENT_PARAM×EVENT_NAME) list"where
          "get_exec_prime s ≡ exec_prime s"
*)

definition get_exec_prime::"State⇒((EVENT_PARAM×EVENT_NAME) list ×TEE_TA_MANAGER × TAs_State)"where
          "get_exec_prime s ≡ (exec_prime s,ta_mgr(TEE_state s),TAs_state s)"

definition is_TEE ::"Sys_Config⇒DOMAIN_ID⇒bool" where
    "is_TEE sc nid ≡ (TEE sc) =nid"

definition is_REE ::"Sys_Config⇒DOMAIN_ID⇒bool" where
    "is_REE sc nid ≡ (REE sc) =nid"

definition is_TA ::"Sys_Config⇒DOMAIN_ID⇒bool" where
    "is_TA sc nid ≡ ¬((TEE sc) =nid ∨ (REE sc) =nid)"




definition interference1 :: "DOMAIN_ID⇒DOMAIN_ID⇒bool"("(_ ↝ _)")where
    "interference1 d1 d2 ≡
                  if d1 = d2 then True
                  else if is_TEE sysconf d1 then True
                  else if is_REE sysconf d1 then False
                  else if is_TA sysconf d1 then False
                  else False"

definition non_interference1 :: "DOMAIN_ID ⇒ DOMAIN_ID ⇒ bool" ("(_ ∖↝ _)")
      where "(u ∖↝  v) ≡ ¬ (u ↝ v)"





definition vpeq_REE :: "State⇒DOMAIN_ID⇒State⇒bool" where
        "vpeq_REE s d t ≡ ree_total_size(REE_state s) = ree_total_size (REE_state t)
                          ∧driver_mem(REE_state s) = driver_mem(REE_state t) "

(*for TA, only memory is sensitive data, including TA data and keys*)
definition vpeq_TA :: "State⇒DOMAIN_ID⇒State⇒bool" where
        "vpeq_TA s d t ≡ {x. x∈set(tee_memories (TEE_state s))∧ (ownership x=d)} =
                           {x. x∈set(tee_memories (TEE_state t))∧ (ownership x=d)}
                       "

(*   ∨{x. x∈set(tee_memories (TEE_state s))∧ (ownership x=d)} ⊆ 
                            {x. x∈set(tee_memories (TEE_state t))∧ (ownership x=d)}
                          ∨{x. x∈set(tee_memories (TEE_state t))∧ (ownership x=d)} ⊆
                            {x. x∈set(tee_memories (TEE_state s))∧ (ownership x=d)}*)


(*for TEE, only memory is sensitive data,including TEE's own execution space*)
(*In TEE side, mem whose blockid equals 0 belongs to TEE*)
definition vpeq_TEE :: "State⇒DOMAIN_ID⇒State⇒bool" where
        "vpeq_TEE s d t ≡ {x. x∈set(tee_memories (TEE_state s))∧ (block_id x=0)} =
                           {x. x∈set(tee_memories (TEE_state t))∧ (block_id x=0)}"


definition vpeq1 :: "State ⇒ DOMAIN_ID ⇒ State ⇒ bool" ("(_ ∼ _ ∼ _)") 
  where "vpeq1 s d t ≡  
         (if d = TEE sysconf then 
            (vpeq_TEE s d t)
          else if d = REE sysconf then
            (vpeq_REE s d t)
          else if is_TA sysconf d then 
            (vpeq_TA s d t)
          else True)"


declare non_interference1_def [cong] and interference1_def [cong] and domain_of_event_def[cong] and
      is_TEE_def[cong] and is_REE_def[cong] and is_TA_def[cong] and vpeq_REE_def[cong] and vpeq_TA_def[cong]
      and vpeq_TEE_def[cong] and vpeq1_def[cong]

(*
declare TEEC_InitializeContext_def[cong] TEEC_FinalizeContext_def[cong] 
TEEC_OpenSession1_def[cong] TEEC_OpenSession2_def[cong] TEEC_OpenSession3_def[cong] TEEC_OpenSession4_def[cong]
TEEC_CloseSession1_def[cong] TEEC_CloseSession2_def[cong] TEEC_CloseSession3_def[cong] TEEC_CloseSession4_def[cong]
TEEC_InvokeCommand1_def[cong] TEEC_InvokeCommand2_def[cong] TEEC_InvokeCommand3_def[cong] TEEC_InvokeCommand4_def[cong]
TEE_OpenTASession1_def[cong] TEE_OpenTASession2_def[cong] TEE_OpenTASession3_def[cong] TEE_OpenTASession4_def[cong]
TEEC_OpenSession1_def[cong] TEEC_OpenSession2_def[cong] TEEC_OpenSession3_def[cong] TEEC_OpenSession4_def[cong]
TEEC_OpenSession1_def[cong] TEEC_OpenSession2_def[cong] TEEC_OpenSession3_def[cong] TEEC_OpenSession4_def[cong]
*)

lemma vpeq_REE_transitive : "∀s r t d. vpeq_REE s d t ∧ vpeq_REE t d r⟶vpeq_REE s d r" 
      by auto

lemma vpeq_REE_symmetric : "∀ s t d. vpeq_REE s d t ⟶ vpeq_REE t d s"
      by auto

lemma vpeq_REE_reflexive:"∀ s d. vpeq_REE s d s"
      by auto

lemma vpeq_TA_transitive : "∀s r t d. vpeq_TA s d t ∧ vpeq_TA t d r⟶vpeq_TA s d r" 
      by auto

lemma vpeq_TA_symmetric : "∀ s t d. vpeq_TA s d t ⟶ vpeq_TA t d s"
      by auto

lemma vpeq_TA_reflexive:"∀ s d. vpeq_TA s d s"
      by auto

lemma vpeq_TEE_transitive : "∀s r t d. vpeq_TEE s d t ∧ vpeq_TEE t d r⟶vpeq_TEE s d r" 
      by auto

lemma vpeq_TEE_symmetric : "∀ s t d. vpeq_TEE s d t ⟶ vpeq_TEE t d s"
      by auto

lemma vpeq_TEE_reflexive:"∀ s d. vpeq_TEE s d s"
      by auto

lemma vpeq1_transitive : "∀s r t d. vpeq1 s d t ∧ vpeq1 t d r⟶vpeq1 s d r" 
      by auto

lemma vpeq1_symmetric : "∀ s t d. vpeq1 s d t ⟶ vpeq1 t d s"
      by auto

lemma vpeq1_reflexive:"∀ s d. vpeq1 s d s"
      by auto

lemma ins_tee_intf_all : "∀d. interference1 (TEE sysconf) d"
      by auto

lemma ins_no_intf_tee : "∀d. interference1 d (TEE sysconf) ⟶d=(TEE sysconf) "
      using interference1_def is_TEE_def by presburger
      
lemma ins_reachable: "∀s a. (O_ISOLATION.reachable0 s0t exec_event) s ⟶ (∃s'. (s, s') ∈ exec_event a)"
  proof -
  {
    fix s a
    assume p0: "(O_ISOLATION.reachable0 s0t exec_event) s"
    have "∃s'. (s, s') ∈ exec_event a"
      proof(induct a)
        case (hyperc x) show ?case 
          apply (induct x)
          by (simp add:exec_event_def)+
        next
        case (sys x) then show ?case
          apply (induct x)
          by (simp add:exec_event_def)+
      qed        
  }
  then show ?thesis by auto
  qed

lemma nintf_neq: "u ∖↝  v ⟹ u ≠ v"  by auto

lemma nintf_reflx: "interference1 u u" by auto

lemma tee_ne_ree: "TEE sysconf ≠REE sysconf"
by (simp add: tee_no_ree)
                                                                       

interpretation O_ISOLATION
        s0t exec_event domain_of_event get_exec_prime vpeq1 interference1 "TEE sysconf" "REE sysconf" TA_domain1
        using   vpeq1_transitive vpeq1_symmetric vpeq1_reflexive ins_tee_intf_all ins_no_intf_tee
             nintf_reflx  ins_reachable
             by (smt (verit, best) O_ISOLATION.intro) 


(*
subsection "CA_TA_IDENTIFICATION Instantiation"

subsection "INSTANCE_TIME Instantiation"

lemma time_mono:"∀s a s'. (s,s')∈exec_event a ⟶system_time s = system_time s'" 
            sorry

interpretation O_INSTANCE_TIME
              getTAInstanceTime exec_event
            using time_mono
            by (simp add: O_INSTANCE_TIME.intro getTAInstanceTime_def) 


subsection "KEYS_USAGE Instantiation"

type_synonym KEY = nat
consts key_checksum::"KEY⇒DOMAIN_ID⇒bool"

interpretation O_KEYS_USAGE 
                key_checksum
               done

subsection "OPERATION Instantiation"

lemma action_correct:"∀s a s' d. (s,s')∈exec_event a ∧ domain_of_event s a ≠d ⟶s=s'"
sorry
*)

subsection "TA_AUTHENTICITY Instantiation"

consts bin_verify::"BIN⇒CHECKCODE⇒bool"
interpretation O_TA_AUTHENTICITY 
                bin_verify
              done

end